Nuprl Lemma : pos_mul_arg_bounds
13,42
postcript
pdf
a
,
b
:
. ((
a
*
b
) > 0)
(((
a
> 0) & (
b
> 0))
((
a
< 0) & (
b
< 0)))
latex
Up
int
2
,
int
2
Definitions
,
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
i
>
j
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
True
,
T
Lemmas
gt
wf
,
int
trichot
,
mul
cancel
in
lt
,
mul
bounds
1b
,
true
wf
,
squash
wf
origin
a, b:
. ((a * b) > 0) 
(((a > 0) & (b > 0)) 
((a < 0) & (b < 0))) a, b:. ((a * b) > 0) (((a > 0) & (b > 0)) ((a < 0) & (b < 0))) 
T Q Q Q Qx:A. B(x)
T